Nuprl Lemma : member-insert
0,22
postcript
pdf
T
:Type,
eq
:EqDecider(
T
),
a
:
T
,
L
:
T
List,
b
:
T
. (
b
insert(
a
;
L
))
b
=
a
(
b
L
)
latex
Definitions
EqDecider(
T
)
,
P
Q
,
P
Q
,
(
x
l
)
,
t
T
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
deq
wf
,
insert
property
origin
T:Type, eq:EqDecider(T), a:T, L:T List, b:T. (b 
insert(a;L)) 
b = a 
(b L) T:Type, eq:EqDecider(T), a:T, L:T List, b:T. (b insert(a;L)) b = a (b L) Q Q l) T
Qx:A. B(x)